Ghosts of Departed Proofs

1つの関数を定義する際に、引数部分を工夫する

その関数を使うための前提条件を幽霊型を用いて表現する

間違った使い方のできない関数を定義し提供することができる

「Ghosts of Departed Proofs」という名前の意味

直訳すると「去りゆく証明の亡霊」

The name “ghost proof” is meant to suggest the related concept of ghost variables in software verification. ref 『Ghosts of Departed Proofs』 1.4

ghost variablesが不明なので正確にはわからないが、以下のようなニュアンスだと思うmrsekut.icon

この手法では、幽霊型を用いて、その型が証明済みであることを表現する

これは、型で表されるので実行時のオーバーヘッドはない

証明が、実体のないものであって、コンパイルの結果には現れないことを強調している

改善？